es:ES, i, x:Id, k:Knd. es-independent(es;i;k;x)  Prop 

latex

Definitions	t  T, x:A. B(x), es-V(es), f(a), es-M(es), act(k), tag(k), lnk(k), isrcv(k), kindtype(i;k), locl(a), rcv(l,tg), x:AB(x), Trans(i), S  T, False, Id, vartype(i;x), state@i, b, islocal(k), x:AB(x), left+right, Knd, ES, Unit, Type, P  Q, Choose(i), s = t, Prop, Send(i), Msg, type List, s1  s2 mod x@i, P & Q, es-independent(es;i;k;x)
Lemmas	es-vartype wf, es-x-equiv wf, es-Msg wf, es-send wf, assert wf, islocal wf, es-choose wf, es-kindtype wf, actof wf, unit wf, Knd wf, Id wf, event system wf, rcv wf, es-trans wf, locl wf, es-M wf, subtype rel self, es-V wf